(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)

(** ** Matrix Module *)
Require Export List.
Require Export Matrix.Mat.Mat_def.
Require Export Matrix.Mat.Mat_make.
Require Export Matrix.Mat.list_function.
Require Export Matrix.Mat.Mat_IO.
Require Export Matrix.Mat.Mat_map.
Require Export Matrix.Mat.Mat_add.
Require Export Matrix.Mat.Mat_sub.
Require Export Matrix.Mat.Mat_trans.
Require Export Matrix.Mat.Mat_mult.
Require Export Matrix.Mat.Mat_mult_lemma.
Require Export Matrix.Mat.Mat_trans_lemma.

Require Export Setoid.
Require Export Relation_Definitions.
Set Implicit Arguments.

(* ################################################################# *)
(** * Definition of Module Type *)

Module Type MType.

Parameter A :Set.
Parameter Zero One : A.
Parameter opp : A -> A.
Parameter add sub mul: A->A->A.

Infix " + " := add.
Infix " - " := sub.
Infix " * " := mul.

Parameter add_comm : forall x y , x + y = y + x.
Parameter add_assoc : forall x y z , x + y + z = x + (y + z).
Parameter add_assoc2 : forall x y z w, (x+y)+(z+w) = (x+z)+(y+w).
Parameter add_zero_l : forall x , Zero + x  = x.
Parameter add_zero_r : forall x , x + Zero = x.

Parameter sub_assoc : forall x y z, x - y - z = x - (y + z).
Parameter sub_assoc2: forall x y z w, (x+y)-(z+w) = (x-z)+(y-w).
Parameter sub_opp : forall x y , x - y = opp (y - x ).
Parameter sub_zero_l:forall x ,Zero - x = opp x.
Parameter sub_zero_r:forall x , x - Zero = x.
Parameter sub_self : forall x , x-x =Zero.

(*Parameter mul_one_l : forall x , One * x = x. *)
Parameter mul_add_distr_l : forall x y z, (x+y)*z = x*z + y*z.
Parameter mul_add_distr_r : forall x y z, x*(y+z) = x*y + x*z.
Parameter mul_sub_distr_l : forall x y z, (x-y)*z = x*z - y*z.
Parameter mul_sub_distr_r : forall x y z, x*(y-z) = x*y - x*z.
Parameter mul_assoc : forall x y z, x * y * z = x * (y * z).
Parameter mul_zero_l : forall x , Zero * x = Zero.
Parameter mul_zero_r : forall x , x * Zero = Zero.
Parameter mul_one_l : forall x , One * x = x.
Parameter mul_comm : forall x y, x*y = y*x.



End MType.

(** * Definition of Matrix Module *)

Module Matrix (M : MType).

Definition A := M.A.

Definition Meq := @M_eq A .
Arguments Meq {m} {n}.

Definition Mtrans := @trans A M.Zero.
Arguments Mtrans {m} {n}.

Definition Madd := @matrix_each A M.add.
Arguments Madd {m} {n}.

Definition Msub := @matrix_each A M.sub.
Arguments Msub {m} {n}. 

Definition Mopp := @matrix_map A M.opp.
Arguments Mopp {m} {n}.

Definition Mmul := @matrix_mul A M.Zero M.add M.mul.
Arguments Mmul {m} {n} {p}.

Definition Mmulc_l:= @const_mul_l A M.mul.
Arguments Mmulc_l {m} {n}.

Definition Mmulc_r:= @const_mul_r A M.mul.
Arguments Mmulc_r {m} {n}.

Definition MO := @MO A M.Zero.

Definition MI := @MI A M.Zero M.One.

Notation "m1 M= m2" := (Meq m1 m2) (at level 70).

Notation "m1 M+ m2" := (Madd m1 m2) (at level 65).

Notation "m1 M- m2" := (Msub m1 m2) (at level 65).

Notation " M- m" := (Mopp m) (at level 65).

Notation "m1 M* m2" := (Mmul m1 m2) (at level 60).

Notation "c C* m" := (Mmulc_l c m) (at level 60).

Notation "m *C c" := (Mmulc_r m c) (at level 60).

Notation "T( m )" := (Mtrans m) (at level 55).

Lemma MMeq_ref : forall {m n:nat}, reflexive _ (@Meq m n).
intros. unfold reflexive. apply M_eq_ref.
Qed.

Lemma MMeq_sym : forall {m n:nat}, symmetric _ (@Meq m n).
intros. unfold symmetric. apply M_eq_sym.
Qed.

Lemma MMeq_trans : forall {m n:nat}, transitive _ (@Meq m n).
intros. unfold transitive. apply M_eq_trans.
Qed.

Add Parametric Relation {m n:nat} : (@Mat M.A m n) (@Meq m n) 
  reflexivity proved by (@MMeq_ref m n)
  symmetry proved by (@MMeq_sym m n)
  transitivity proved by (@MMeq_trans m n)
  as MMeq_rel.
(*
Lemma Madd_compat : 
  forall m n, 
     forall x x' : (@MMat m n), @Meq m n x x' ->
     forall y y' : (@MMat m n), @Meq m n y y' ->
         @Meq m n (Madd x y) (Madd x' y').
Proof.
  intros.
  unfold Madd,Meq. unfold Meq in H.
  unfold Meq in H0. unfold matrix_each,mat_each,M_eq.
  simpl. rewrite H. rewrite H0. reflexivity.
Qed.

Add Parametric Morphism {m n :nat}: (@Madd m n)
  with signature (@Meq m n) ==> (@Meq m n) ==> (@Meq m n) 
  as Madd_mor.
Proof.
exact (@Madd_compat m n).
Qed.
*)
(** ** A + B = B + A *)

Lemma Madd_comm : forall {m n:nat} (ma mb:Mat M.A m n) ,
  ma M+ mb M=  mb M+ ma.
Proof.
  intros.
  apply matrix_comm.
  apply M.add_comm.
Qed.

(** ** A + B + C = A + ( B + C) *)

Lemma Madd_assoc : forall{m n:nat} (ma mb mc:Mat M.A m n) , 
  (ma M+ mb) M+ mc M=
  ma M+ (mb M+ mc).
Proof.
  intros. apply matrix_assoc.
  apply M.add_assoc.
Qed.



(** ** O + A = A *)

Lemma Madd_zero_l : forall {m n:nat} (ma:Mat M.A m n) , 
  ((MO m n) M+ ma) M= ma.
Proof.
  intros.
  apply matrix_add_zero_l.
  intros.
  rewrite M.add_comm.
  apply M.add_zero_r.
Qed.

(** ** A + O = A *)

Lemma Madd_zero_r : forall {m n:nat} (ma:Mat M.A m n) , 
  (ma M+ (MO m n)) M=  ma.
Proof.
  intros.
  rewrite Madd_comm.
  apply Madd_zero_l.
Qed.

(** ** A - B = - ( B - A ) *)

Lemma Msub_comm : forall {m n:nat} (m1 m2:Mat M.A m n) , 
  m1 M- m2 M= M- (m2 M- m1).
Proof.
  intros.
  apply matrix_sub_opp with(negative:=M.opp).
  apply M.sub_opp.
Qed.

(** ** A - B - C = A - ( B + C ) *)

Lemma Msub_assoc : forall {m n:nat} (m1 m2 m3:Mat M.A m n) , 
  (m1 M- m2) M- m3 M=
  m1 M- (m2 M+ m3).
Proof.
  intros.
  apply matrix_sub_assoc.
  apply M.sub_assoc.
Qed.

(** ** O - A = - A *)

Lemma Msub_O_l : forall {m n:nat} (m1 :Mat M.A m n),
  (MO m n) M- m1 M= M- m1.
Proof.
  intros.
  apply matrix_sub_zero_l.
  apply M.sub_zero_l.
Qed.

(** ** A - O = A *)

Lemma Msub_O_r:forall {m n:nat} (m1 :Mat M.A m n),
  m1 M- (MO m n)  M= m1.
Proof.
  intros.
  apply matrix_sub_zero_r.
  apply M.sub_zero_r.
Qed.

(** ** A - A = O *)

Lemma Msub_self : forall {m n:nat} (m1 :Mat M.A m n),
  m1 M- m1 M= MO m n.
Proof.
  intros.
  apply matrix_sub_self.
  apply M.sub_self.
Qed.

(** ** ( A + B ) * C = A * C + B * C *)

Lemma Mmul_add_distr_l : forall {m n p:nat} (ma mb :Mat M.A m n)
  (mc :Mat M.A n p),
  (ma M+ mb) M* mc M= ma M* mc M+ mb M* mc.
Proof.
  intros. apply matrix_mul_distr_l.
  apply M.add_zero_r. intros. apply M.add_assoc2.
  apply M.mul_add_distr_l.
Qed.

(** ** A * ( B + C ) = A * B + A * C *)
Lemma Mmul_add_distr_r :  forall {m n p:nat} (ma :Mat M.A m n)
  (mb mc :Mat M.A n p),
   ma M* (mb M+ mc) M= ma M* mb M+ ma M* mc.
Proof.
  intros. apply matrix_mul_distr_r.
  apply M.add_zero_r. apply M.add_assoc2. apply M.mul_add_distr_r.
Qed.

Lemma Mmul_sub_distr_l : forall {m n p:nat} (ma mb :Mat M.A m n)
  (mc :Mat M.A n p),
  (ma M- mb) M* mc M= ma M* mc M- mb M* mc.
Proof.
  intros. apply matrix_mul_distr_l.
  apply M.sub_zero_r. intros. apply M.sub_assoc2.
  apply M.mul_sub_distr_l.
Qed.

(** ** A * ( B + C ) = A * B + A * C *)
Lemma Mmul_sub_distr_r :  forall {m n p:nat} (ma :Mat M.A m n)
  (mb mc :Mat M.A n p),
   ma M* (mb M- mc) M= ma M* mb M- ma M* mc.
Proof.
  intros. apply matrix_mul_distr_r.
  apply M.sub_zero_r. apply M.sub_assoc2. apply M.mul_sub_distr_r.
Qed.

(** ** A * B * C = A * ( B *  C ) *)
Lemma Mmul_assoc: forall {m n p k} (ma:Mat M.A m n)(mb:Mat M.A n p)
  (mc:Mat M.A p k),
  ma M* mb M* mc M= ma M* (mb M* mc).
Proof.
  intros. apply matrix_mul_assoc.
  apply M.add_zero_r. intros.
  apply M.mul_assoc. apply M.mul_zero_r.
  apply M.mul_zero_l. apply M.add_zero_l.
  apply M.mul_add_distr_r. intros. apply M.mul_comm.
  apply M.mul_add_distr_l. apply M.add_assoc2.
Qed.

(** ** O * A = O *)
Lemma Mmul_zero_l: forall {m n:nat} (ma:Mat M.A m n) ,
  (MO m m) M* ma M= (MO m n).
Proof.
  intros. apply matrix_mul_zero_l.
  apply M.mul_zero_l. apply M.add_zero_l.
Qed.

(** ** A * O = O *)
Lemma Mmul_zero_r: forall {m n:nat} (ma:Mat M.A m n) ,
  ma M* (MO n n) M= (MO m n).
Proof.
  intros. apply matrix_mul_zero_r.
  apply M.mul_comm. apply M.mul_zero_r.
  apply M.add_zero_l.
Qed.

(** ** I * A = A *)

Lemma Mmul_unit_l : forall{m n:nat} (ma:Mat M.A m n) , 
  (MI m) M* ma M= ma.
Proof.
  intros.
  apply matrix_mul_unit_l.
  apply M.mul_one_l. apply M.add_zero_r.
  apply M.mul_zero_l. apply M.add_zero_l.
Qed.

(** ** A * I = A *)

Lemma Mmul_unit_r : forall {m n:nat} (ma:Mat M.A m n) , 
  ma M* (MI n) M= ma.
Proof.
  intros.
  apply matrix_mul_unit_r.
  apply M.mul_one_l. apply M.add_zero_r.
  apply M.mul_zero_l. apply M.add_zero_l.
  apply M.mul_comm.
Qed.

(** ** c * A = A * c *)

Lemma Mmulc_comm: forall {m n:nat}c1(ma:Mat M.A m n),
  c1 C* ma M= c1 *C ma.
Proof.
  intros.
  apply const_mul_comm.
  apply M.mul_comm.
Qed.

(** ** c * ( A + B ) = c * A + c * B *)

Lemma Mmulc_distr_l: forall {m n:nat} c (ma1 ma2:Mat M.A m n),
   c C* (ma1 M+ ma2) M= c C* ma1 M+ c C* ma2.
Proof.
  intros.
  apply const_mul_l_distr_r.
  apply M.mul_add_distr_r.
Qed.

(** ** 0 * A = O *)

Lemma Mmulc_0_l:forall  {m n:nat}(ma:Mat M.A m n),
  M.Zero C* ma M= MO m n.
Proof.
  intros.
  apply const_mul_l_0.
  apply M.mul_zero_l.
Qed.


Lemma Meq_teq: forall {m n:nat} (ma mb:Mat M.A m n),
  ma M= mb <-> T( ma ) M= T( mb ).
Proof.
  intros. apply meq_teq.
Qed.

(** ** T( T( A ) ) = A *)

Lemma Mtteq : forall {m n:nat} (ma:Mat M.A m n) , 
  T(T(ma)) M= ma.
Proof.
  intros.
  apply trans_same;auto.
  apply mat_height. apply mat_width.
Qed.

(** ** T( c * A ) = c * T(A) *)

Lemma Mcteq : forall {m n:nat} c (ma:Mat M.A m n),
  T(c C* ma) M= c C* T(ma).
Proof.
  intros.
  apply cteq.
  apply M.mul_zero_r.
Qed.

(** ** T( A + B ) = T( A ) + T( B ) *)

Lemma Mteq_add: forall {m n :nat} (ma mb:Mat M.A m n ),
  T(ma M+ mb) M= T(ma) M+ T(mb).
Proof.
  intros.
  apply teq_add.
  apply M.add_zero_r.
Qed.

(** ** T( A - B ) = T( A ) - T( B ) *)

Lemma Mteq_sub: forall {m n :nat} (ma mb:Mat M.A m n ),
  T(ma M- mb) M= T(ma) M- T(mb).
Proof.
  intros.
  apply teq_add.
  apply M.sub_zero_r.
Qed.


(** ** T( A * B ) = T( B ) * T( B ) *)

Lemma Mteq_mul: forall {m n p:nat} (ma:Mat M.A m n)(mb:Mat M.A n p),
  T(ma M* mb) M= T(mb) M* T(ma).
Proof.
  intros.
  apply teq_mul.
  apply M.add_zero_l.
  apply M.mul_comm.
Qed.

Lemma Mtrans_MI: forall {n:nat},
  T(MI n) M= MI n.
Proof.
  apply trans_MI.
Qed.

End Matrix.

